(set-logic QF_BV)
(declare-fun x () (_ BitVec 16))
(declare-fun y () (_ BitVec 15))
(declare-fun z () (_ BitVec 15))
(declare-fun w () (_ BitVec 1))
(assert 
  (let ((e6 (bvnot x))) 
  (let ((e7 (bvand z y))) 
  (let ((e8 (bvmul e6 ((_ sign_extend 1) e7)))) 
  (let ((e11 ((_ zero_extend 14) w))) 
  (let ((e24 (bvslt ((_ sign_extend 1) e11) e8))) 
  (let ((e42 (xor e24 false))) 
  (let ((e45 (= false e42))) 
  (let ((e59 (=> true e45))) 
  (let ((e64 (= true e59))) 
  (let ((e65 (or e64 e64))) 
  (let ((e66 (ite e65 false true))) 
  (let ((e67 e66)) 
  (let ((e68 e67)) e68))))))))))))))
(check-sat)

